(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const r0 Real)
(declare-const r1 Real)
(declare-const r2 Real)
(declare-const r3 Real)
(declare-const r13 Real)
(declare-const r14 Real)
(declare-const r18 Real)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const r19 Real)
(declare-const r20 Real)
(declare-const r21 Real)
(declare-const v14 Bool)
(declare-const r22 Real)
(declare-const v16 Bool)
(declare-const r23 Real)
(declare-const r24 Real)
(assert (or (xor v6 v11 v12 v0 (< 540.0 r2) v11 (and v5 v7 v2 v3 v10 v3) v9 (not v6)) (distinct (distinct 0.3978788865 r19 r2 4364548.0 0.45) v1 v8)))
(assert (or (distinct (- 0.3978788865) 0.45 (/ 43969.00 4364548.0) (- r14 540.0 4364548.0))))
(assert (or (and v5 v7 v2 v3 v10 v3)))
(assert (or v6))
(check-sat)
